/*
 * DIMACSParser.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef DIMACSPARSER_HPP_
#define DIMACSPARSER_HPP_

#include <iostream>
#include <string>

#include "bfr/Clause.hpp"
#include "bfr/ClauseSet.hpp"

namespace bfr {

/**
 * A parser to read ClauseSet objects from a DIMACS input.
 *
 * The DIMACS file format is widely used to describe CNFs.
 * For a description of the DIMACS format see
 * <a href="http://logic.pdmi.ras.ru/~basolver/dimacs.html">
 * here</a>.
 *
 * This class can parse DIMACS cnf problems from an istream.
 *
 */
class DIMACSParser {

    public:

        /**
         * The problem type defined in the problem line.
         */
        enum problem_type {
            CNF, /*!<CNF (conjunctive normal form) problem. */
            UNKNOWN /*!< Something else. */
        };

        /**
         * Constructor.
         */
        DIMACSParser();

        /**
         * Destructor.
         */
        ~DIMACSParser();

        /**
         * Parse a clause set from an istream.
         *
         * The method will expect to read a problem line,
         * if does not find one an exception will be thrown.
         *
         * After the problem line it will read exactly
         * as many clauses as defined in the problem lines
         * (comment lines between the clauses are allowed).
         *
         * @throw std::string If the stream does not contain a valid DIMACS
         * instance.
         */
        ClauseSet *parse(std::istream &in) throw(std::string);

        /**
         * Returns the number of variables in the last parsed input.
         *
         * This method returns 0 if no DNF has been parsed yet.
         *
         * @return Number of variables in the last parsed input.
         */
        size_t getVariableCount() const;

        /**
         * The comment character ('c').
         */
        static const char COMMENT_CHAR;

        /**
         * The problem line character ('p').
         */
        static const char PROBLEM_CHAR;

        /**
         * Minus character ('-').
         */
        static const char MINUS;

        /**
         * CNF problem as string ("cnf").
         */
        static const char CNF_PROBLEM[];

    private:
        size_t variableCount;
        size_t clauseCount;
        ClauseSet *clauses;
        problem_type type;

        void readProblemLine(std::string &line) throw(std::string);
        size_t parseNumber(std::string &line, size_t *pos) throw(std::string);
        Clause *readClause(std::string &line) throw(std::string);
        inline bool isLineEmpty(const std::string &line) const;

};

}

#endif  // DIMACSPARSER_HPP_
